Nuprl Lemma : sqequal_1 13,42

COM: sqequal_1_begin

COM: sqequal_com

COM: sq_type_com

ABS: SQType(T)

STM: int sq

STM: nat sq

STM: bool sq

STM: atom sq

COM: case_ite_com

STM: bool sim true

STM: bool sim false

STM: eq int eq true intro

STM: eq int eq false intro

STM: lt int eq true elim

STM: lt int eq false elim

STM: eq atom eq true elim

STM: eq atom eq false elim

STM: eq int eq true elim sqequal

STM: eq int eq false elim sqequal

STM: lt int eq true elim sqequal

STM: lt int eq false elim sqequal

STM: eq atom eq true elim sqequal

STM: eq atom eq false elim sqequal

STM: bool cases sqequal

COM: sqequal_1_end


UpStandard, Standard

origin